What if there is a library function that writes a property that can be read later.
Shouldn't the step type be configurable to support that case?

Yes, all of our additional step mechanisms have this limitation, and we should totally fix that. I've often wanted to do something about this, but so far I haven't been able to find a robust way to do it right.

Concretely, the API should not restrict future implementation changes too much, and should be applied consistently across all the additional step mechanisms. Adding a step summary as an extra parameter might work here, but if we try the same in data-flow configurations, we will quickly run out of possible ways to overload this predicate, as we already have overloads using flow-labels as extra parameters.

OK. Lets start with this version then, perhaps with a docstring warning about the default choice of flowstep (which all the other additional step mechanism also need).

The TaintFunction API in the C++ library is a fairly nice way of supporting a special, but common, case of this. We're also using it for Go, and I think we should explore having something like it for JavaScript. (Though we'd probably have to attach the models to function calls, not the functions themselves, since we don't have those for most framework functions.)